T:Type. 
subtype_rel(T; )
 (as:(T List). 
 (sorted(as)  no_repeats(T; as))
  (i:int_seg(0; ||as||), j:int_seg(0; i). as[j] < as[i])) 

latex

Definitions	t  T, x:A. B(x), ||as||, P  Q, lelt(i; j; k), P  Q, False, A, A  B, int_seg(i; j), subtype(S; T), l[i], no_repeats(T; l), sorted(L), prop{i:l}, P  Q, P  Q, ge(i; j), , guard(T), sq_type(T), P  Q, decidable(P)
Lemmas	not wf, nat wf, decidable lt, le wf, sorted wf, no repeats wf, int seg wf, select wf, length wf1